Nuprl Lemma : rng_times_nat_op_r
11,40
postcript
pdf
r
:Rng,
a
,
b
:|
r
|,
n
:
. ((
n
r
b
) *
a
) = (
n
r
(
b
*
a
))
|
r
|
latex
Definitions
t
T
,
n
x(
op
;
id
)
e
,
n
e
,
n
r
e
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
False
,
A
,
A
B
,
P
Q
,
Rng
,
x
(
s
)
,
,
(
r
)
i
k
<
j
.
E
(
k
)
,
lb
i
<
ub
.
E
(
i
)
Lemmas
rng
wf
,
rng
car
wf
,
nat
wf
,
int
seg
wf
,
rng
times
sum
r
origin
r:Rng, a, b:|r|, n:
. ((n 
r b) * a) = (n r (b * a)) 
|r| r:Rng, a, b:|r|, n:. ((n r b) * a) = (n r (b * a)) |r| T er ex:A. B(x)
x. t(x)
A
B
Q
(r) i k < j. E(k)
lb i < ub. E(i)